STM: band-to-and

STM: bor-to-and

STM: bnot-tt

STM: bnot-ff

ABS: bool-decider(b)

STM: bool-decider wf

ABS: projn(n;x)

ABS: invert-union(x)

STM: invert-union wf

STM: not-false

STM: not-true

STM: not-assert

STM: not-not-assert

STM: equal-bnot

STM: inconsistent-bool-eq

STM: inconsistent-bool-eq2

STM: inconsistent-bool-eq3

STM: inconsistent-bool-eq4

ABS: [d]

STM: dcdr-to-bool wf

STM: dcdr-to-bool-equivalence

STM: test-rewrite-dcdr

STM: bool-to-dcdr-aux

STM: bool-to-neg-dcdr-aux

ABS: {f}

STM: bool-to-neg-dcdr wf

ABS: {f}

STM: bool-to-dcdr wf

ABS: if p:P then A(p) else B fi 

STM: branch wf

STM: branch wf2

STM: branch-ifthenelse

STM: decidable-filter

ABS: can-apply(f;x)

STM: can-apply wf

ABS: do-apply(f;x)

STM: do-apply wf

STM: inl-do-apply

ABS: f o g  

STM: p-compose wf

ABS: f o' g

STM: p-compose' wf

ABS: p-lift(d;f)

STM: p-lift wf

STM: can-apply-p-lift

STM: do-apply-p-lift

STM: can-apply-compose-sq

STM: can-apply-compose

STM: can-apply-compose-iff

STM: do-apply-compose

STM: can-apply-compose'

STM: do-apply-compose'

ABS: p-id()

STM: p-id wf

STM: p-compose-id

STM: p-id-compose

STM: p-compose-associative

ABS: p-first(L)

STM: p-first wf

STM: p-first-singleton

ABS: p first nil compseq tag def

ABS: [f?g]

STM: p-conditional wf

STM: p-conditional-domain

STM: p-conditional-to-p-first

ABS: p-filter(f)

STM: p-filter wf

ABS: p-co-filter(f)

STM: p-co-filter wf

STM: can-apply-p-filter

STM: can-apply-p-co-filter

STM: do-apply-p-filter

STM: do-apply-p-co-filter

ABS: p-restrict(f;p)

STM: p-restrict wf

ABS: p-co-restrict(f;p)

STM: p-co-restrict wf

STM: can-apply-p-restrict

STM: can-apply-p-co-restrict

STM: do-apply-p-restrict

STM: do-apply-p-co-restrict

ABS: f^n

STM: p-fun-exp wf

STM: p-fun-exp-one

STM: p-fun-exp-compose

STM: p-fun-exp-add

STM: can-apply-fun-exp-add

STM: can-apply-fun-exp-add-iff

STM: simple-primrec-add

STM: p-fun-exp-add1-sq

STM: can-apply-fun-exp

STM: p-fun-exp-add-sq

ABS: p-mu(P;x)

STM: p-mu wf

STM: p-mu-exists

STM: p-mu-decider

ABS: mu'(P)

STM: mu' wf

STM: can-apply-mu'

STM: do-apply-mu'

STM: member-assert

STM: length wf nat

STM: hd member

ABS: fseg(T;L1;L2)

STM: fseg wf

STM: nth tl is fseg

STM: member nth tl

STM: nth tl append

STM: fseg append

STM: fseg extend

STM: fseg transitivity

STM: fseg weakening

STM: nil fseg

STM: fseg nil

STM: fseg length

STM: filter fseg

STM: fseg member

STM: fseg select

ABS: lastn(n;L)

STM: lastn wf

STM: length-lastn

ABS: adjacent(T;L;x;y)

STM: adjacent wf

STM: adjacent-nil

STM: adjacent-singleton

STM: adjacent-cons

STM: simplify-equal-imp

STM: equal-top

ABS: p-inject(A;B;f)

STM: p-inject wf

STM: p-compose-inject

STM: p-fun-exp-injection

STM: subtype-top

STM: subtype rel-equal

STM: subtype rel self

STM: fun exp add-sq

STM: decidable implies better

STM: subtype rel function

STM: subtype rel dep function

STM: subtype rel dep function iff

STM: subtype rel product

STM: subtype rel dep product iff

STM: subtype rel sum

STM: subtype rel set

STM: subtype rel list

STM: subtype rel transitivity

ABS: A r B

STM: rev subtype rel wf

ABS: A  B

STM: ext-eq wf

STM: ext-eq weakening

STM: ext-eq inversion

STM: ext-eq transitivity

STM: subtype rel functionality wrt iff

STM: subtype rel functionality wrt implies

STM: subtype rel weakening

STM: rev subtype rel weakening

STM: list-subtype

STM: nil member-variant

STM: member-exists

STM: member-exists2

STM: sub-equality

STM: l all wf2

STM: null-ite

STM: typed-null-ite

STM: decidable equal union

STM: decidable equal unit

STM: length-append

STM: filter-commutes

STM: null wf3

STM: member-zip

STM: adjacent-append

STM: adjacent-before

STM: adjacent-member

STM: adjacent-sublist

STM: hd-before

STM: before-hd

STM: last-not-before

STM: before-adjacent

STM: before-adjacent2

STM: adjacent-to-same

STM: adjacent-to-same-sublist

STM: adjacent-to-same-sublist2

STM: adjacent-to-last

STM: no repeats-sublist

STM: sublist-same-last

STM: decidable equal product

STM: decidable equal nat plus

STM: decidable equal nat

STM: member-decide-assert

STM: filter wf2

STM: no repeats filter2

STM: filter tt

STM: filter type2

STM: filter wf3

STM: general-append-cancellation

STM: append-cancellation

STM: append-impossible

STM: append-impossible2

STM: append-cancellation-right

STM: append iseg

STM: iseg append iff

STM: iseg append single

STM: iseg append length

STM: list accum append

STM: last induction

STM: last-cons

STM: last append

STM: list accum functionality

STM: list accum filter

STM: p-first-append

STM: p-first-cons

STM: can-apply-p-first

STM: do-apply-p-first

ABS: p-disjoint(A;f;g)

STM: p-disjoint wf

STM: compat-iff-common-iseg

ABS: A  B

STM: l contains wf

STM: l contains weakening

STM: l contains nil

STM: nil-contains

STM: l contains cons

STM: l contains append

STM: l contains append2

STM: l contains append3

STM: l contains-append4

STM: l contains disjoint

STM: l disjoint append

STM: l disjoint append2

STM: l disjoint-symmetry

STM: l disjoint singleton

STM: l disjoint singleton2

STM: l disjoint nil

STM: l disjoint nil2

ABS: xL.P(x)

STM: l-all wf

ABS: f[x:=v]

STM: update wf

ABS: l[i:=x]

STM: list update wf

STM: list update select

STM: list update length

STM: iseg antisymmetry

STM: compat-cons

STM: compat-append

STM: compat-append2

STM: compat symmetry

STM: compat-iseg

STM: compat-iseg2

ABS: sorted-by(R;L)

STM: sorted-by wf

ABS: sorted(L)

STM: sorted wf

STM: sorted-cons

STM: sorted-by-cons

STM: sorted-filter

ABS: insert-by(eq;r;x;l)

STM: insert-by wf

ABS: s-insert(x;l)

STM: s-insert wf

STM: member-s-insert

STM: member-insert-by

STM: s-insert-sorted

STM: insert-by-sorted-by

STM: s-insert-no-repeats

STM: insert-by-no-repeats

STM: sorted-by-exists

STM: sorted-by-exists2

ABS: s-filter(p;as)

STM: s-filter wf

ABS: merge(as;bs)

STM: merge wf

STM: member-merge

STM: sorted-merge

STM: no repeats-merge

STM: strict-sorted

ABS: priority-select(f;g;as)

STM: priority-select wf

STM: priority-select-property

STM: priority-select-inr

STM: not-isl-priority-select

STM: priority-select-tt

STM: priority-select-ff

STM: fun exp add sq

STM: all-but-one

STM: no repeats member

ABS: imax-list(L)

STM: imax-list wf

STM: imax-list-ub

STM: imax-list-lb

STM: imax-list-subset

STM: subset-map

STM: maximal-in-list

STM: member-le-max

STM: l member subtype

STM: l member subtype2

STM: l all-nil

STM: l all iff

STM: l all subtype

ABS: l_interval(l;j;i)

STM: l interval wf

STM: length l interval

STM: select l interval

STM: hd l interval

STM: last l interval

ABS: (x,yL.  P(x;y))

STM: pairwise wf

STM: pairwise-nil

STM: pairwise-singleton

STM: pairwise-cons

STM: do-apply-p-first-disjoint

ABS: inv-rel(A;B;f;finv)

STM: inv-rel wf

STM: inv-rel-inject

STM: hd-filter

STM: find-hd-filter

STM: list-set-type

STM: list-set-type-property

STM: list-set-type-member

STM: list-set-type2

STM: list-set-type3

STM: list-equal-set

STM: l member set

STM: l member set2

STM: l member-set

STM: member map2

STM: no-repeats-pairwise

STM: member-mapfilter

STM: mapfilter-append

STM: map-wf2

STM: wellfounded-anti-reflexive

STM: no-member-sq-nil

STM: l before append iff

STM: append assoc sq

STM: append-nil

STM: nil-iff-no-member

STM: tl sublist

ABS: dectt(d)

STM: dectt wf

STM: assert-dectt

STM: inr equal

STM: inl equal

STM: inl eq inr

STM: inr eq inl

ABS: finite-type(T)

STM: finite-type wf

STM: finite-type-iff-list

STM: finite-type-bool

STM: finite-set-type

STM: finite-decidable-set

STM: finite-subtype

STM: map-map

STM: map is nil

STM: map-id

STM: length-map

STM: length-map-sq

STM: select-map

STM: pairwise-map

STM: pairwise-map2

STM: general length nth tl

STM: nth tl nil

ABS: mu(f)

STM: mu wf

STM: mu-wf2

STM: mu-property

STM: mu-property2

STM: mu-bound

STM: mu-bound-property

STM: mu-bound-property+

STM: mu-bound-unique

ABS: upto(n)

STM: upto wf

STM: length upto

STM: upto is nil

STM: upto decomp

STM: upto iseg

STM: select upto

STM: member upto

STM: member upto2

STM: before-upto

STM: list-eq-set-type

STM: before-map

STM: filter append sq

STM: filter map upto

STM: filter map upto2

STM: member-firstn

STM: first0

STM: firstn decomp2

STM: append firstn lastn sq

STM: last-lemma-sq

STM: last-map

STM: firstn firstn

STM: firstn last

STM: firstn append

STM: firstn length

STM: firstn all

STM: firstn map

STM: firstn upto

STM: map is append

STM: map is cons

STM: decidable-last-rel

STM: decidable-exists-iseg

STM: decidable l exists better-extract

STM: decidable l all-better-extract

STM: first-iseg

STM: iseg-transition-lemma

ABS: concat(ll)

STM: concat wf

STM: concat append

STM: concat-cons

STM: concat-nil

STM: map-concat

STM: filter-concat

STM: select concat

STM: member-concat

STM: l member decomp

STM: concat-decomp

STM: last-concat

STM: concat iseg

STM: concat map upto

STM: concat-is-nil

STM: finite-type-product

STM: finite-type-union

STM: finite-type-unit

ABS: star-append(T;P;Q)

STM: star-append wf

STM: star-append-iff

STM: finite-set-type-cases

ABS: mapl(f;l)

STM: mapl wf

STM: member-mapl

STM: pairwise-mapl

STM: pairwise-mapl-no-repeats

STM: no repeats map

STM: no repeats-append

STM: member-reverse

STM: no repeats reverse

STM: length-reverse

STM: reverse-append

STM: reverse-reverse

STM: sublist-reverse

STM: last-reverse

STM: hd-reverse

STM: adjacent-reverse

ABS: CV(F)

STM: CV wf

STM: CV property

ABS: b = accum(z,x.f(z;x),a,{xX|P(x)})

STM: accum filter rel wf

STM: accum filter rel nil

STM: concat-map-decide

STM: map-decide

STM: concat-map-map-decide

STM: void-list-equality

STM: void-list-equality2

STM: void-list-equality3

STM: equal-nil-lists

ABS: SWellFounded(R(x;y))

STM: strongwellfounded wf

STM: strongwf-implies

STM: strongwf-monotone

ABS: p-graph(A;f)

STM: p-graph wf

STM: p-graph wf2

ABS: final-iterate(f;x)

STM: final-iterate wf

STM: final-iterate-property

STM: same-final-iterate-one-one

ABS: R|P

STM: rel-restriction wf

STM: rel-restriction-implies

STM: restriction-of-transitive

STM: restriction-to-field

ABS: R^+

STM: rel plus wf

STM: rel plus trans

STM: rel plus strongwellfounded

STM: rel plus implies

STM: rel plus implies2

STM: rel exp iff

STM: rel exp iff2

STM: rel exp one

STM: rel plus closure

STM: rel star iff

STM: rel star iff2

STM: rel-star-iff-rel-plus-or

ABS: rel-path(R;L)

STM: rel-path wf

ABS: rel-path-between(T;R;x;y;L)

STM: rel-path-between wf

STM: rel-path-between-cons

STM: rel exp-iff-path

STM: rel star-iff-path

STM: rel-rel-plus

STM: rel-star-rel-plus

STM: rel-star-rel-plus2

STM: rel-plus-rel-star

STM: rel plus iff

STM: rel plus iff2

STM: rel plus monotone

STM: rel plus functionality wrt rel implies

STM: rel star functionality wrt rel implies

STM: rel exp functionality wrt rel implies

STM: rel plus functionality wrt brle

STM: rel star functionality wrt brle

STM: rel exp functionality wrt brle

STM: rel plus functionality wrt breqv

STM: rel star functionality wrt breqv

STM: rel exp functionality wrt breqv

STM: rel plus minimal

STM: rel plus idempotent

STM: rel exp functionality wrt iff

STM: rel plus functionality wrt iff

STM: rel plus field

STM: rel plus-of-restriction

STM: rel plus-restriction-equiv

ABS: one-one(A;B;R)

STM: one-one wf

STM: rel exp-one-one

STM: rel-exp-add-iff

STM: map-upto-length

STM: filter-equals

STM: implies-filter-equal

ABS: l-ordered(T;x,y.R(x;y);L)

STM: l-ordered wf

STM: no repeats-before-equality

STM: l-ordered-no repeats

STM: no repeats-permute

STM: l member-permute

STM: split-at-first

STM: l-ordered-equality

STM: transitive-loop

STM: transitive-loop2

ABS: Generic{f:T|S(f)}

STM: generic wf

STM: generic-non-empty

STM: pair-coding-exists

STM: finite-sequence-coding-exists

STM: generic-countable-intersection

ABS: |a/b - p/q| < 1/m

STM: ratio-dist wf

ABS: size(k;f)

STM: bool-size wf

ABS: #{i<j|f i eq x}

STM: seq-count wf

ABS: frequency(f;x) ~ (p/q)

STM: frequency wf

ABS: derived-seq(f;s)

STM: derived-seq wf

ABS: eq_seq(eq)

STM: eq seq wf

ABS: exp(i;n)

STM: exp wf

ABS: let a,b,c,d,e,f,g,h = u in v(a;b;c;d;e;f;g;h)

STM: decidable wellfound-bounded-exists

STM: wellfounded-minimal

STM: wellfounded-minimal-field

STM: closure-well-founded-total

ABS: R!

STM: rel-immediate wf

STM: rel-immediate functionality wrt iff

STM: rel-immediate functionality wrt breqv

STM: rel-plus-rel-immediate

STM: rel-immediate-rel-plus

STM: rel-immediate-exists

ABS: sum_of_torder(T;R)

STM: rel-is-immediate

STM: sum of torder wf

STM: rel-immediate-property

STM: rel-immediate-preserves-order

STM: mutual-primitive-recursion

ABS:  A ~ B

STM: equipollent wf

STM: equipollent weakening

STM: equipollent inversion

STM: equipollent transitivity

STM: product functionality wrt equi[pollent left

STM: product functionality wrt equipollent right

STM: equipollent functionality wrt equipollent

STM: function functionality wrt equipollent left

STM: function functionality wrt equipollent right

STM: equipollent interval

STM: equipollent-multiply

STM: equipollent-zero

STM: equipollent-void-domain

STM: equipollent-exp

ABS: P1  P2

STM: predicate or wf

ABS: P1  P2

STM: predicate implies wf

ABS: P1  P2

STM: predicate rev implies wf

ABS: P1  P2

STM: predicate equivalent wf

STM: predicate equivalent implies

STM: predicate implies weakening

STM: predicate rev implies weakening

STM: predicate equivalent weakening

STM: predicate implies reflexivity

STM: predicate implies transitivity

STM: predicate equivalent transitivity

STM: predicate equivalent inversion

STM: predicate or idempotent

STM: rel or-restriction

ABS: R1  R2

STM: rel equivalent wf

STM: rel equivalent weakening

STM: rel implies weakening

STM: rel implies transitivity

STM: rel equivalent transitivity

STM: rel equivalent inversion

ABS: R1  R2

STM: rel rev implies wf

STM: rel rev implies weakening

STM: rel implies functionality

STM: rel or idempotent

ABS: y=f*(x) via L

STM: fun-path wf

STM: fun-path-member

STM: fun-path-cons

STM: fun-path-fixedpoint

STM: fun-path-append

ABS: y is f*(x)

STM: fun-connected wf

STM: fun-connected-induction

STM: fun-path-induction

ABS: y = f+(x)

STM: strict-fun-connected wf

STM: strict-fun-connected irreflexivity

STM: fun-connected weakening eq

STM: fun-connected weakening

STM: fun-connected-step

STM: fun-connected-step-back

STM: strict-fun-connected-step

STM: strict-fun-connected-induction

STM: fun-connected transitivity

STM: fun-connected-test

STM: fun-connected-tree

STM: fun-connected-fixedpoint

STM: fun-path-member-connected

STM: fun-path-before

ABS: retraction(T;f)

STM: retraction wf

STM: retraction-fun-path

STM: fun-connected antisymmetry

STM: strict-fun-connected transitivity1

STM: strict-fun-connected transitivity2

STM: strict-fun-connected transitivity3

STM: fun-path-no repeats

STM: retraction-fun-path-before

STM: retraction-fixedpoint

STM: strong-fun-connected-induction

STM: decidable fun-connected

STM: between-fun-connected